/*
 * SplitResult.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef SPLITRESULT_HPP_
#define SPLITRESULT_HPP_

#include <vector>

#include "bfr/ClauseSet.hpp"
#include "bfr/OccurrencePattern.hpp"

namespace bfr {

/**
 * Elements of this class are returned in the methods
 * SplittingTreeNode#splitAway and SplittingTreeNode#splitBoth.
 *
 * It encapsulates some information about the result of splitting
 * away a variable.
 *
 * It stores:
 * <ul>
 *      <li>Of the the resulting DNF (#getDNF)</li>
 *      <li>A vector containing the occurrence patterns of this DNF
 *          (#getOccurrences)</li>
 *      <li>The information if the DNF is final, i. e. if it represents
 *          <i>true</i> or <i>false</i> (#isFinal).</li>
 * </ul>
 */
class SplitResult {
	public:
                /**
                 * Constructor.
                 *
                 * @param final <code>true</code>
                 * if the DNF is <i>true</i> or <i>false</i>.
                 * @param dnf The DNF.
                 * @param occurrences The occurrence patterns for the DNF.
                 */
		SplitResult(bool final, ClauseSet *dnf,
				std::vector<OccurrencePattern*> *occurrences);
		/**
		 * Destructor.
		 *
		 * Deletes nothing.
		 */
		virtual ~SplitResult();

		/**
		 * Check whether the DNF is <i>true</i> or <i>false</i>.
		 *
		 * @return <code>true</code> if the DNF is <i>true</i> or
		 * <i>false</i>.
		 */
		bool isFinal() const;

		/**
		 * Return the DNF.
		 *
		 * @return The DNF.
		 */
		ClauseSet *getDNF() const;

		/**
		 * Return the occurrence patterns for the DNF.
		 *
		 * @return the occurrence patterns for the DNF.
		 */
		std::vector<OccurrencePattern*> *getOccurrences() const;

	private:
		bool final;
		ClauseSet *dnf;
		std::vector<OccurrencePattern*> *occurrences;
};

} /* namespace bfr */
#endif /* SPLITRESULT_HPP_ */
